(declare-sort aa 0) 

(declare-sort f 0) 

(declare-sort ab 0) 

(declare-sort o 0) 

(declare-fun g () ab)
(declare-fun h (aa ab) c)
(declare-fun i (aa ab) ab)
(declare-fun ac (aa ab) ab)
(declare-fun an (ab) Int)
(declare-fun ar (ab ab) ab)
(declare-fun idisjoint (ab ab) c)
(assert (forall ((a ab)) (= (idisjoint a g) d)))
(assert (forall ((a ab) (b ab)) (= (idisjoint a b) (idisjoint b a))))
(assert (forall ((e aa)) (not (= (h e g) d))))
(assert (forall ((k aa) (l aa) (m ab)) (= (h k (i l m)) (ite (or (= (h k m) d)) d Falsity))))
(assert (forall ((k aa) (l aa) (m ab)) (= (h k (ac l m)) (ite (and (not (= k l)) (= (h k m) d)) d Falsity))))
(assert (forall ((k aa) (a ab)) (=> (= (h k a) d) (forall ((b ab)) (= (h k (ar a b)) d)))))
(assert (forall ((a ab) (b ab)) (= (ar a b) (ar b a))))
(assert (forall ((k aa) (a ab) (b ab)) (=> (= (h k (ar a b)) d) (or (= (h k b) d)))))
(assert (forall ((a ab)) (= (ar a a) a)))
(assert (forall ((a ab)) (= (ar a g) a)))
(assert (forall ((a ab) (b ab)) (=> (= (ar a b) g) (= a g))))
(assert (forall ((m ab)) (=> (= (an m) 0) (= m g))))
(assert (forall ((m ab)) (>= (an m) 0)))
(assert (forall ((k aa) (m ab)) (= (an (i k m)) (ite (= (h k m) d) 0 (+ (an m) 1)))))
(assert (forall ((k aa) (m ab)) (= (an (ac k m)) (ite (= (h k m) d) 0 (an m)))))
(assert (forall ((a ab) (b ab)) (=> (= (idisjoint a b) d) (= 0 0))))
(declare-fun iac (ab ab) c)
(assert (forall ((a ab) (b ab)) (=> (exists ((k aa)) (= (h k a) (h k b))) (= (iac a b) d))))
(declare-fun qaa () o)
(declare-fun p (f o) c)
(declare-fun q (f o) o)
(declare-fun ql (f o) o)
(declare-fun qcardinality (o) Int)
(declare-fun qunion (o o) o)
(declare-fun qdisjoint (o o) c)
(assert (forall ((a o)) (= (qdisjoint a qaa) d)))
(assert (forall ((a o) (b o)) (= (qdisjoint a b) (qdisjoint b a))))
(assert (forall ((k f) (l f) (m o)) (= (p k (q l m)) (ite (or (distinct k l)) d Falsity))))
(assert (forall ((k f) (l f) (m o)) (= (p k (ql l m)) (ite (or (not (= k l))) d Falsity))))
(assert (forall ((k f) (a o)) (=> (= (p k a) d) (forall ((b o)) (= (p k (qunion a b)) d)))))
(assert (forall ((a o) (b o)) (= (qunion a b) (qunion b a))))
(assert (forall ((k f) (a o) (b o)) (=> (= (p k (qunion a b)) d) (or (= (p k b) d)))))
(assert (forall ((a o)) (= (qunion a a) a)))
(assert (forall ((a o)) (= (qunion a qaa) a)))
(assert (forall ((a o) (b o)) (=> (= (qunion a b) qaa) (= a qaa))))
(assert (= (qcardinality qaa) 0))
(assert (forall ((m o)) (=> (= (qcardinality m) 0) (= m qaa))))
(assert (forall ((m o)) (>= (qcardinality m) 0)))
(assert (forall ((k f) (m o)) (= (qcardinality (q k m)) (ite (= (p k m) d) (qcardinality m) (+ (qcardinality m) 1)))))
(assert (forall ((k f) (m o)) (= (qcardinality (ql k m)) (ite (= (p k m) d) (- (qcardinality m) 1) (qcardinality m)))))
(assert (forall ((a o) (b o)) (=> (= (qdisjoint a b) d) (= (qcardinality (qunion a b)) (+ (qcardinality a) (qcardinality b))))))
(declare-fun qac (o o) c)
(assert (forall ((a o) (b o)) (= (qac a b) (ite (= a b) d Falsity))))
(assert (exists ((a o) (b o)) (= (forall ((k f)) (= (p k a) (p k b))) (distinct (qac a b) d))))
(declare-fun r () (Array aa c))
(assert (forall ((s aa)) (= (select r s) Falsity)))
(declare-fun ad () (Array aa c))
(assert (forall ((t aa)) (= (select ad t) Falsity)))
(declare-fun u () (Array aa (Array aa c)))
(assert (forall ((v aa)) (= (select u v) ad)))
(declare-fun w () (Array aa c))
(assert (exists ((ae aa)) (= (select w ae) d)))
(declare-fun y () (Array aa (Array aa c)))
(assert (forall ((x aa)) (= (select y x) w)))
(declare-fun j () Int)
(assert (> j 0))
(declare-fun ag () (Array aa o))
(assert (exists ((ah aa)) (= (select ag ah) af)))
(declare-fun aj () (Array aa o))
(assert (forall ((ak aa)) (= (select aj ak) ai)))
(declare-fun al (o) f)
(assert (forall ((am o)) (or (distinct (p (al am) am) d))))
(declare-fun chosen () (Array aa c))
(declare-fun phase () ang)
(declare-fun asm () aa)
(declare-fun asn () aa)
(declare-fun clean () arg)
(declare-fun at () (Array aa o))
(declare-fun au () (Array aa (Array aa o)))
(declare-fun z () o)
(declare-fun aw () (Array aa (Array aa c)))
(declare-fun ax () Int)
(declare-fun ay () (Array aa (Array aa c)))
(declare-fun azba1 () o)
(declare-fun ay1 () (Array aa (Array aa c)))
(assert (not (=> (and (forall ((n aa)) (=> (= (select chosen n) d) (and (and (not (= phase init_phase))) (>= ax 0)))) (=> (>= ax (+ j 1)) (not (= clean before)))) (=> (= phase ao) (=> (not (= (select (select ay asn) asm) d)) (=> (= azba1 (select at asn)) (=> (= z azba1) (=> (= au (store au asn (store (select au asn) asm (ite (= (select (select aw asn) asm) d) z af)))) (and (= ay1 (store ay asn (store (select ay asn) asm d))) (forall ((n aa)) (=> (= (select chosen n) d) (and (and (not (distinct clean before)) (not (= phase init_phase))) (>= ax (+ j 1))))))))))))))
(check-sat)
